$\forall$${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$), $l$:IdLnk, ${\it tg}$:Id.
\\[0ex](es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]$\Rightarrow$ guard(((loc($e$) = destination($l$) $\in$ Id) $\wedge$ (loc(es{-}sender(${\it es}$; $e$)) = source($l$) $\in$ Id)))